00100	OP
00200	←(V1,A1)
00300	NIL
00400	NIL
00500	NIL
00600	ISVAR(V1);;
00700	C(V1,A1);;
00800	
00900	
01000	ITERATIVE
01100	TUNIFY
01200	NIL
01300	NIL
01400	NIL
01500	NEWVAR(V7);NEWVAR(V8);NEWVAR(V12);NEWVAR(V13);
01600	VUNIFY(V4,V5,V6);
01700	C(V12 V1);C(V13 V2);C(V3,V4);C(V7,V5);C(V8,V6);;
01800	C(V3,V9);C(V7,V10);C(V8,V11);C(V12,V14);C(V13,V15);
01900	VUNIFY(V9,V10,V11);;
02000	CUNIFY1(V3 V9 (CAR V14)(CAR V15));
02100	C(V7, (CONS V10, (CAR V14)));C(V8,(CONS V11, (CAR V15)));
02200	C(V12, (CDR V14));C(V13, (CDR V15));;
02300	=(V14,NIL);;
02400	UNIFY(V3 V1 V2);;
02500	UNIFY(V3 V1 V2);;
02600	
02700	OP
02800	VARVAR(V3,V9,T1,T2)
02900	NIL
03000	NIL
03100	NIL
03200	VAR(T1);VAR(T2);;
03300	CUNIFY1(V3,V9,T1,T2);C(V3,(CONS(CONS T1,T2),V9));;
03400	
03500	AXIOM
03600	TAUNIFY
03700	NIL
03800	T
03900	NIL
04000	=(V10,V11);;
04100	VUNIFY(V9,V10,V11);;
04200	
04300	
04400	NIL
04500	NIL
04600	
04700	ISVAR(Z);VAR(A);VAR(B);VUNIFY(NIL NIL NIL);;
04800	
04900	T
05000	
05100	((C T NIL NIL (X,*))
05200	(VAR T T NIL NIL)
05300	(= T NIL NIL NIL)
05400	(CUNIFY T NIL NIL NIL )
05500	(CUNIFY1 T NIL NIL NIL)
05600	(VUNIFY T NIL NIL NIL)
05700	(UNIFY T NIL NIL NIL))
05800	
05900	
06000	
06100	NIL
06200